YES 1.5110000000000001
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ BR
mainModule Main
| ((notElem :: (Eq b, Eq a) => Either b a -> [Either b a] -> Bool) :: (Eq a, Eq b) => Either b a -> [Either b a] -> Bool) |
module Main where
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
| ((notElem :: (Eq b, Eq a) => Either b a -> [Either b a] -> Bool) :: (Eq b, Eq a) => Either b a -> [Either b a] -> Bool) |
module Main where
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
mainModule Main
| (notElem :: (Eq b, Eq a) => Either b a -> [Either b a] -> Bool) |
module Main where
Haskell To QDPs
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(xv2000), Succ(xv4001000)) → new_primPlusNat(xv2000, xv4001000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(xv2000), Succ(xv4001000)) → new_primPlusNat(xv2000, xv4001000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(xv30100), Succ(xv400100)) → new_primMulNat(xv30100, Succ(xv400100))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(xv30100), Succ(xv400100)) → new_primMulNat(xv30100, Succ(xv400100))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(xv3000), Succ(xv40000)) → new_primEqNat(xv3000, xv40000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(xv3000), Succ(xv40000)) → new_primEqNat(xv3000, xv40000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, cc), cd), app(app(ty_@2, de), df)), hd) → new_esEs3(xv302, xv4002, de, df)
new_esEs2(Right(xv30), Right(xv400), bcc, app(ty_[], bcd)) → new_esEs(xv30, xv400, bcd)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(ty_Either, fg), fh), cd, dh) → new_esEs2(xv300, xv4000, fg, fh)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, cc), app(ty_Maybe, ed)), dh), hd) → new_esEs1(xv301, xv4001, ed)
new_esEs1(Just(xv300), Just(xv4000), app(app(app(ty_@3, gd), ge), gf)) → new_esEs0(xv300, xv4000, gd, ge, gf)
new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), app(ty_[], bba), bbb) → new_esEs(xv300, xv4000, bba)
new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), app(app(app(ty_@3, bbc), bbd), bbe), bbb) → new_esEs0(xv300, xv4000, bbc, bbd, bbe)
new_esEs2(Left(xv30), Left(xv400), app(app(ty_Either, he), hf), hd) → new_esEs2(xv30, xv400, he, hf)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), cc, cd, app(ty_[], ce)) → new_esEs(xv302, xv4002, ce)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(ty_[], fa)), cd), dh), hd) → new_esEs(xv300, xv4000, fa)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, app(ty_Maybe, bbf)), bbb), hd) → new_esEs1(xv300, xv4000, bbf)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, cc), cd), app(app(app(ty_@3, cf), cg), da)), hd) → new_esEs0(xv302, xv4002, cf, cg, da)
new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), hg, app(ty_[], hh)) → new_esEs(xv301, xv4001, hh)
new_esEs2(Left(Just(xv300)), Left(Just(xv4000)), app(ty_Maybe, app(ty_Maybe, gg)), hd) → new_esEs1(xv300, xv4000, gg)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(app(ty_@2, ga), gb)), cd), dh), hd) → new_esEs3(xv300, xv4000, ga, gb)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(app(ty_Either, fg), fh)), cd), dh), hd) → new_esEs2(xv300, xv4000, fg, fh)
new_esEs1(Just(xv300), Just(xv4000), app(app(ty_Either, gh), ha)) → new_esEs2(xv300, xv4000, gh, ha)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(ty_Maybe, ff)), cd), dh), hd) → new_esEs1(xv300, xv4000, ff)
new_esEs2(Left(:(xv300, xv301)), Left(:(xv4000, xv4001)), app(ty_[], app(ty_Maybe, bf)), hd) → new_esEs1(xv300, xv4000, bf)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(ty_@2, ga), gb), cd, dh) → new_esEs3(xv300, xv4000, ga, gb)
new_esEs1(Just(xv300), Just(xv4000), app(ty_[], gc)) → new_esEs(xv300, xv4000, gc)
new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), hg, app(ty_Maybe, bad)) → new_esEs1(xv301, xv4001, bad)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, cc), cd), app(ty_[], ce)), hd) → new_esEs(xv302, xv4002, ce)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, app(app(app(ty_@3, bbc), bbd), bbe)), bbb), hd) → new_esEs0(xv300, xv4000, bbc, bbd, bbe)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, app(app(ty_@2, bca), bcb)), bbb), hd) → new_esEs3(xv300, xv4000, bca, bcb)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), cc, app(ty_[], dg), dh) → new_esEs(xv301, xv4001, dg)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, cc), app(app(ty_@2, eg), eh)), dh), hd) → new_esEs3(xv301, xv4001, eg, eh)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, app(ty_[], bba)), bbb), hd) → new_esEs(xv300, xv4000, bba)
new_esEs2(Left(:(xv300, xv301)), Left(:(xv4000, xv4001)), app(ty_[], ba), hd) → new_esEs(xv301, xv4001, ba)
new_esEs2(Right(xv30), Right(xv400), bcc, app(app(ty_Either, bda), bdb)) → new_esEs2(xv30, xv400, bda, bdb)
new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), app(app(ty_@2, bca), bcb), bbb) → new_esEs3(xv300, xv4000, bca, bcb)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, hg), app(ty_Maybe, bad)), hd) → new_esEs1(xv301, xv4001, bad)
new_esEs1(Just(xv300), Just(xv4000), app(ty_Maybe, gg)) → new_esEs1(xv300, xv4000, gg)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, cc), app(app(ty_Either, ee), ef)), dh), hd) → new_esEs2(xv301, xv4001, ee, ef)
new_esEs2(Left(:(xv300, xv301)), Left(:(xv4000, xv4001)), app(ty_[], app(app(ty_@2, ca), cb)), hd) → new_esEs3(xv300, xv4000, ca, cb)
new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), hg, app(app(app(ty_@3, baa), bab), bac)) → new_esEs0(xv301, xv4001, baa, bab, bac)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), cc, cd, app(app(ty_Either, dc), dd)) → new_esEs2(xv302, xv4002, dc, dd)
new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), app(app(ty_Either, bbg), bbh), bbb) → new_esEs2(xv300, xv4000, bbg, bbh)
new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), hg, app(app(ty_Either, bae), baf)) → new_esEs2(xv301, xv4001, bae, baf)
new_esEs2(Left(Just(xv300)), Left(Just(xv4000)), app(ty_Maybe, app(app(ty_Either, gh), ha)), hd) → new_esEs2(xv300, xv4000, gh, ha)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), cc, app(ty_Maybe, ed), dh) → new_esEs1(xv301, xv4001, ed)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), cc, cd, app(app(ty_@2, de), df)) → new_esEs3(xv302, xv4002, de, df)
new_esEs2(Left(Just(xv300)), Left(Just(xv4000)), app(ty_Maybe, app(ty_[], gc)), hd) → new_esEs(xv300, xv4000, gc)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, cc), cd), app(ty_Maybe, db)), hd) → new_esEs1(xv302, xv4002, db)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, cc), app(app(app(ty_@3, ea), eb), ec)), dh), hd) → new_esEs0(xv301, xv4001, ea, eb, ec)
new_esEs2(Left(:(xv300, xv301)), Left(:(xv4000, xv4001)), app(ty_[], app(app(app(ty_@3, bc), bd), be)), hd) → new_esEs0(xv300, xv4000, bc, bd, be)
new_esEs2(Right(xv30), Right(xv400), bcc, app(app(app(ty_@3, bce), bcf), bcg)) → new_esEs0(xv30, xv400, bce, bcf, bcg)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, app(app(ty_Either, bbg), bbh)), bbb), hd) → new_esEs2(xv300, xv4000, bbg, bbh)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, hg), app(ty_[], hh)), hd) → new_esEs(xv301, xv4001, hh)
new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), app(ty_Maybe, bbf), bbb) → new_esEs1(xv300, xv4000, bbf)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), cc, app(app(app(ty_@3, ea), eb), ec), dh) → new_esEs0(xv301, xv4001, ea, eb, ec)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, hg), app(app(app(ty_@3, baa), bab), bac)), hd) → new_esEs0(xv301, xv4001, baa, bab, bac)
new_esEs2(Right(xv30), Right(xv400), bcc, app(app(ty_@2, bdc), bdd)) → new_esEs3(xv30, xv400, bdc, bdd)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), cc, app(app(ty_@2, eg), eh), dh) → new_esEs3(xv301, xv4001, eg, eh)
new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), hg, app(app(ty_@2, bag), bah)) → new_esEs3(xv301, xv4001, bag, bah)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, cc), app(ty_[], dg)), dh), hd) → new_esEs(xv301, xv4001, dg)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(ty_[], fa), cd, dh) → new_esEs(xv300, xv4000, fa)
new_esEs1(Just(xv300), Just(xv4000), app(app(ty_@2, hb), hc)) → new_esEs3(xv300, xv4000, hb, hc)
new_esEs(:(xv300, xv301), :(xv4000, xv4001), ba) → new_esEs(xv301, xv4001, ba)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), cc, cd, app(ty_Maybe, db)) → new_esEs1(xv302, xv4002, db)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), cc, cd, app(app(app(ty_@3, cf), cg), da)) → new_esEs0(xv302, xv4002, cf, cg, da)
new_esEs(:(xv300, xv301), :(xv4000, xv4001), app(app(ty_Either, bg), bh)) → new_esEs2(xv300, xv4000, bg, bh)
new_esEs2(Left(:(xv300, xv301)), Left(:(xv4000, xv4001)), app(ty_[], app(app(ty_Either, bg), bh)), hd) → new_esEs2(xv300, xv4000, bg, bh)
new_esEs2(Left(:(xv300, xv301)), Left(:(xv4000, xv4001)), app(ty_[], app(ty_[], bb)), hd) → new_esEs(xv300, xv4000, bb)
new_esEs(:(xv300, xv301), :(xv4000, xv4001), app(app(app(ty_@3, bc), bd), be)) → new_esEs0(xv300, xv4000, bc, bd, be)
new_esEs2(Right(xv30), Right(xv400), bcc, app(ty_Maybe, bch)) → new_esEs1(xv30, xv400, bch)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, cc), cd), app(app(ty_Either, dc), dd)), hd) → new_esEs2(xv302, xv4002, dc, dd)
new_esEs(:(xv300, xv301), :(xv4000, xv4001), app(app(ty_@2, ca), cb)) → new_esEs3(xv300, xv4000, ca, cb)
new_esEs2(Left(Just(xv300)), Left(Just(xv4000)), app(ty_Maybe, app(app(ty_@2, hb), hc)), hd) → new_esEs3(xv300, xv4000, hb, hc)
new_esEs2(Left(Just(xv300)), Left(Just(xv4000)), app(ty_Maybe, app(app(app(ty_@3, gd), ge), gf)), hd) → new_esEs0(xv300, xv4000, gd, ge, gf)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(ty_Maybe, ff), cd, dh) → new_esEs1(xv300, xv4000, ff)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, hg), app(app(ty_Either, bae), baf)), hd) → new_esEs2(xv301, xv4001, bae, baf)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), cc, app(app(ty_Either, ee), ef), dh) → new_esEs2(xv301, xv4001, ee, ef)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, hg), app(app(ty_@2, bag), bah)), hd) → new_esEs3(xv301, xv4001, bag, bah)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(app(app(ty_@3, fb), fc), fd)), cd), dh), hd) → new_esEs0(xv300, xv4000, fb, fc, fd)
new_esEs(:(xv300, xv301), :(xv4000, xv4001), app(ty_[], bb)) → new_esEs(xv300, xv4000, bb)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(app(ty_@3, fb), fc), fd), cd, dh) → new_esEs0(xv300, xv4000, fb, fc, fd)
new_esEs(:(xv300, xv301), :(xv4000, xv4001), app(ty_Maybe, bf)) → new_esEs1(xv300, xv4000, bf)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_esEs(:(xv300, xv301), :(xv4000, xv4001), app(app(ty_Either, bg), bh)) → new_esEs2(xv300, xv4000, bg, bh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(xv300, xv301), :(xv4000, xv4001), app(app(app(ty_@3, bc), bd), be)) → new_esEs0(xv300, xv4000, bc, bd, be)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(Just(xv300), Just(xv4000), app(app(ty_Either, gh), ha)) → new_esEs2(xv300, xv4000, gh, ha)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Just(xv300), Just(xv4000), app(app(app(ty_@3, gd), ge), gf)) → new_esEs0(xv300, xv4000, gd, ge, gf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(:(xv300, xv301), :(xv4000, xv4001), app(ty_Maybe, bf)) → new_esEs1(xv300, xv4000, bf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(Just(xv300), Just(xv4000), app(ty_Maybe, gg)) → new_esEs1(xv300, xv4000, gg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(xv300, xv301), :(xv4000, xv4001), app(app(ty_@2, ca), cb)) → new_esEs3(xv300, xv4000, ca, cb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Just(xv300), Just(xv4000), app(app(ty_@2, hb), hc)) → new_esEs3(xv300, xv4000, hb, hc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Just(xv300), Just(xv4000), app(ty_[], gc)) → new_esEs(xv300, xv4000, gc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), app(app(ty_Either, bbg), bbh), bbb) → new_esEs2(xv300, xv4000, bbg, bbh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), hg, app(app(ty_Either, bae), baf)) → new_esEs2(xv301, xv4001, bae, baf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), app(app(app(ty_@3, bbc), bbd), bbe), bbb) → new_esEs0(xv300, xv4000, bbc, bbd, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), hg, app(app(app(ty_@3, baa), bab), bac)) → new_esEs0(xv301, xv4001, baa, bab, bac)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), hg, app(ty_Maybe, bad)) → new_esEs1(xv301, xv4001, bad)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), app(ty_Maybe, bbf), bbb) → new_esEs1(xv300, xv4000, bbf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), app(app(ty_@2, bca), bcb), bbb) → new_esEs3(xv300, xv4000, bca, bcb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), hg, app(app(ty_@2, bag), bah)) → new_esEs3(xv301, xv4001, bag, bah)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), app(ty_[], bba), bbb) → new_esEs(xv300, xv4000, bba)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), hg, app(ty_[], hh)) → new_esEs(xv301, xv4001, hh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(Left(xv30), Left(xv400), app(app(ty_Either, he), hf), hd) → new_esEs2(xv30, xv400, he, hf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(app(ty_Either, fg), fh)), cd), dh), hd) → new_esEs2(xv300, xv4000, fg, fh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Right(xv30), Right(xv400), bcc, app(app(ty_Either, bda), bdb)) → new_esEs2(xv30, xv400, bda, bdb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, cc), app(app(ty_Either, ee), ef)), dh), hd) → new_esEs2(xv301, xv4001, ee, ef)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(Just(xv300)), Left(Just(xv4000)), app(ty_Maybe, app(app(ty_Either, gh), ha)), hd) → new_esEs2(xv300, xv4000, gh, ha)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, app(app(ty_Either, bbg), bbh)), bbb), hd) → new_esEs2(xv300, xv4000, bbg, bbh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(:(xv300, xv301)), Left(:(xv4000, xv4001)), app(ty_[], app(app(ty_Either, bg), bh)), hd) → new_esEs2(xv300, xv4000, bg, bh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, cc), cd), app(app(ty_Either, dc), dd)), hd) → new_esEs2(xv302, xv4002, dc, dd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, hg), app(app(ty_Either, bae), baf)), hd) → new_esEs2(xv301, xv4001, bae, baf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(ty_Either, fg), fh), cd, dh) → new_esEs2(xv300, xv4000, fg, fh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), cc, cd, app(app(ty_Either, dc), dd)) → new_esEs2(xv302, xv4002, dc, dd)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), cc, app(app(ty_Either, ee), ef), dh) → new_esEs2(xv301, xv4001, ee, ef)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(:(xv300, xv301), :(xv4000, xv4001), ba) → new_esEs(xv301, xv4001, ba)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_esEs(:(xv300, xv301), :(xv4000, xv4001), app(ty_[], bb)) → new_esEs(xv300, xv4000, bb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, cc), cd), app(app(app(ty_@3, cf), cg), da)), hd) → new_esEs0(xv302, xv4002, cf, cg, da)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, app(app(app(ty_@3, bbc), bbd), bbe)), bbb), hd) → new_esEs0(xv300, xv4000, bbc, bbd, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, cc), app(app(app(ty_@3, ea), eb), ec)), dh), hd) → new_esEs0(xv301, xv4001, ea, eb, ec)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Left(:(xv300, xv301)), Left(:(xv4000, xv4001)), app(ty_[], app(app(app(ty_@3, bc), bd), be)), hd) → new_esEs0(xv300, xv4000, bc, bd, be)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Right(xv30), Right(xv400), bcc, app(app(app(ty_@3, bce), bcf), bcg)) → new_esEs0(xv30, xv400, bce, bcf, bcg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, hg), app(app(app(ty_@3, baa), bab), bac)), hd) → new_esEs0(xv301, xv4001, baa, bab, bac)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Left(Just(xv300)), Left(Just(xv4000)), app(ty_Maybe, app(app(app(ty_@3, gd), ge), gf)), hd) → new_esEs0(xv300, xv4000, gd, ge, gf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(app(app(ty_@3, fb), fc), fd)), cd), dh), hd) → new_esEs0(xv300, xv4000, fb, fc, fd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, cc), app(ty_Maybe, ed)), dh), hd) → new_esEs1(xv301, xv4001, ed)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, app(ty_Maybe, bbf)), bbb), hd) → new_esEs1(xv300, xv4000, bbf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(Just(xv300)), Left(Just(xv4000)), app(ty_Maybe, app(ty_Maybe, gg)), hd) → new_esEs1(xv300, xv4000, gg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(ty_Maybe, ff)), cd), dh), hd) → new_esEs1(xv300, xv4000, ff)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(:(xv300, xv301)), Left(:(xv4000, xv4001)), app(ty_[], app(ty_Maybe, bf)), hd) → new_esEs1(xv300, xv4000, bf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, hg), app(ty_Maybe, bad)), hd) → new_esEs1(xv301, xv4001, bad)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, cc), cd), app(ty_Maybe, db)), hd) → new_esEs1(xv302, xv4002, db)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Right(xv30), Right(xv400), bcc, app(ty_Maybe, bch)) → new_esEs1(xv30, xv400, bch)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, cc), cd), app(app(ty_@2, de), df)), hd) → new_esEs3(xv302, xv4002, de, df)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(app(ty_@2, ga), gb)), cd), dh), hd) → new_esEs3(xv300, xv4000, ga, gb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, app(app(ty_@2, bca), bcb)), bbb), hd) → new_esEs3(xv300, xv4000, bca, bcb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, cc), app(app(ty_@2, eg), eh)), dh), hd) → new_esEs3(xv301, xv4001, eg, eh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(:(xv300, xv301)), Left(:(xv4000, xv4001)), app(ty_[], app(app(ty_@2, ca), cb)), hd) → new_esEs3(xv300, xv4000, ca, cb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Right(xv30), Right(xv400), bcc, app(app(ty_@2, bdc), bdd)) → new_esEs3(xv30, xv400, bdc, bdd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(Left(Just(xv300)), Left(Just(xv4000)), app(ty_Maybe, app(app(ty_@2, hb), hc)), hd) → new_esEs3(xv300, xv4000, hb, hc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, hg), app(app(ty_@2, bag), bah)), hd) → new_esEs3(xv301, xv4001, bag, bah)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Right(xv30), Right(xv400), bcc, app(ty_[], bcd)) → new_esEs(xv30, xv400, bcd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(ty_[], fa)), cd), dh), hd) → new_esEs(xv300, xv4000, fa)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, cc), cd), app(ty_[], ce)), hd) → new_esEs(xv302, xv4002, ce)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, app(ty_[], bba)), bbb), hd) → new_esEs(xv300, xv4000, bba)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(:(xv300, xv301)), Left(:(xv4000, xv4001)), app(ty_[], ba), hd) → new_esEs(xv301, xv4001, ba)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(Just(xv300)), Left(Just(xv4000)), app(ty_Maybe, app(ty_[], gc)), hd) → new_esEs(xv300, xv4000, gc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv4000, xv4001)), app(app(ty_@2, hg), app(ty_[], hh)), hd) → new_esEs(xv301, xv4001, hh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, cc), app(ty_[], dg)), dh), hd) → new_esEs(xv301, xv4001, dg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(:(xv300, xv301)), Left(:(xv4000, xv4001)), app(ty_[], app(ty_[], bb)), hd) → new_esEs(xv300, xv4000, bb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), cc, app(app(app(ty_@3, ea), eb), ec), dh) → new_esEs0(xv301, xv4001, ea, eb, ec)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), cc, cd, app(app(app(ty_@3, cf), cg), da)) → new_esEs0(xv302, xv4002, cf, cg, da)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(app(ty_@3, fb), fc), fd), cd, dh) → new_esEs0(xv300, xv4000, fb, fc, fd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), cc, app(ty_Maybe, ed), dh) → new_esEs1(xv301, xv4001, ed)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), cc, cd, app(ty_Maybe, db)) → new_esEs1(xv302, xv4002, db)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(ty_Maybe, ff), cd, dh) → new_esEs1(xv300, xv4000, ff)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(ty_@2, ga), gb), cd, dh) → new_esEs3(xv300, xv4000, ga, gb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), cc, cd, app(app(ty_@2, de), df)) → new_esEs3(xv302, xv4002, de, df)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), cc, app(app(ty_@2, eg), eh), dh) → new_esEs3(xv301, xv4001, eg, eh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), cc, cd, app(ty_[], ce)) → new_esEs(xv302, xv4002, ce)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), cc, app(ty_[], dg), dh) → new_esEs(xv301, xv4001, dg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(ty_[], fa), cd, dh) → new_esEs(xv300, xv4000, fa)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_foldr(xv3, :(xv40, xv41), ba, bb) → new_foldr(xv3, xv41, ba, bb)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldr(xv3, :(xv40, xv41), ba, bb) → new_foldr(xv3, xv41, ba, bb)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3, 4 >= 4